es:event_system{i:l}, e,e':es-E(es). (e = e')  sqequal([e, e']; cons(e'; [])) 

latex

Definitions	x:A. B(x), P  Q, [e, e'], t  T, prop{i:l}, l_all(L; T; x.P(x)), x(s), A, sq_type(T), guard(T), False, append(as; bs), filter(P; l), Y, reduce(f; k; as), if b then t else f fi , tt, ff, P  Q, P  Q, P  Q, , Unit,
Lemmas	filter append, es-ble wf, es-before wf, es-E wf, event system wf, filter is nil, not functionality wrt iff, assert wf, es-le wf, assert-es-ble, l member wf, member-es-before, es-locl transitivity2, es-le weakening eq, es-locl irreflexivity, filter wf, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot